Complete verification of system implementations is a daunting task, if not infeasible for complex real-world systems. Software model checking directly model checks the implementation of a target system, and hence, avoids the error-prone phase of transforming the system implementation into the abstract model. Software model checking is able to find some rare bugs for some existing software systems. However, the large scale software systems (e.g., distributed systems) tend to be complicated and lead to a huge state space for a software model checker to explore. Thus, state space explosion is a major obstacle to the effectiveness of these model checkers.
Compositional reasoning techniques have been proposed to mitigate the state space explosion problem by decoupling the complex software system into components and eagerly construct interface processes to simulate behaviors of the environment for each component. With interface process, it model-checks each component respectively to make sure that it satisfies some properties, and then borrows human effort to reason the correctness of the whole system that includes these components. Unfortunately, the construction of interface process is not practical for real complex software system. The needs for human interference also decrease the effectiveness of such techniques significantly.